(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(set-logic ALL)
(define-fun f9 ((v99 String)(v9c String))Bool (str.<= v99 (str.at v9c 0))
)
(declare-fun v36f() String)
(declare-fun v372() String)
(assert (not (f9 v36f v372)))
(assert (= "\xccS'\xe7\xeakv\xc8=\xebN\xaf\x13Z\xb9\x09\xd5*\x9e&\xbf\x8a\xe0\xeb\xc0\x17t\xb1\xee\xd6\x1a\xcd\xd0\x07\xce\xba\xcd\xc3\x93!\x8a\x19\x16\xed\x16\x82\xdd\x18\xb9\x83\x8e\xa3\xcd\x91\xb6\xb3" v36f))
(assert (= "\xccS'\xe7\xeakv\xc8=\xebN\xaf\x13Z\xb9\x09\xd5*\x9e&\xbf\x8a\xe0\xeb\xc0\x17t\xb1\xee\xd6\x1a\xcd\xd0\x07\xce\xba\xcd\xc3\x93!\x8a\x19\x16\xed\x16\x82\xdd\x18\xb9\x83\x8e\xa3\xcd\x91\xb6\xb3" v372))
(check-sat)
(exit)
